The present invention relates generally to digital circuit design verification, and more particularly to formal verification across differing circuit architectures.
In the design of digital integrated circuits, it is often desirable to be able to ascertain whether two circuits are equivalent. Equivalency of two combinational circuits can be defined, in a functional sense, as follows. A first design and a second design are equivalent if both accept the same set of input combinations, and if both produce the same output combination for each input combination.
The determination of circuit equivalency has become increasingly important with the emergence of large scale digital integrated circuits that incorporate an entire system on a chip. Such chips have reached a size and complexity level where it is difficult to verify them, in a timely manner, using traditional gate-level simulation. As a result, static verification tools are being more widely utilized by chip designers. Examples of such static-verification tools are PrimeTime, a static-timing analyzer, and Formality, a formal verification tool. Both PrimeTime and Formality are products of Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Static-timing analysis is used to analyze and verify the timing of the design and formal verification is used to verify a design""s functionality by proving functional equivalence.
A design methodology that utilizes formal verification can reduce the number of time-consuming gate-level simulation runs. In a typical design process, utilizing logic synthesis and formal verification tools, the designer specifies his or her initial design at the register-transfer level (RTL). This RTL source specification is translated into a gate-level netlist by a logic synthesis tool, such as Design Compiler, produced by Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Formal verification is then used to compare the functional equivalency of the RTL source specification to the post-synthesis gate-level netlist. This gate-level netlist may then undergo several succeeding transformations that are intended to produce equivalent gate-level netlists. Such succeeding transformations can include: scan chain insertion, clock-tree synthesis, in-place optimization and manual editing. After each of these succeeding transformations, formal verification can be used to verify that the result of the latest transformation is functionally equivalent to the resulting gate-level netlist of the preceding transformation. For each of these comparisons a known-to-be-correct design (reference design) is compared against a design of unknown correctness (implementation design).
While formal equivalence checkers generally provide better coverage than gate-level simulation, such formal equivalency checking is fundamentally an NP-complete problem and therefore existing algorithms do not use reasonable memory or CPU resources for certain classes of circuits.
For example, (binary decision diagrams) BDDs have been successfully used for formal equivalency checking, but there are many functions for which the size of the BDD is exponential with respect to the size of the circuit being verified. This is most commonly known to occur with multiplier circuits. BDDs are generally incapable of verifying multipliers with more than sixteen bits in the multiplicands.
Other approaches to formal equivalency checking utilize the fact that (as discussed above) the implementation circuit is derived directly from the reference circuit through synthesis. Because of this, the two circuits usually have a great deal of structural similarity. Certain verification algorithms take advantage of this similarity by trying to find internal equivalence points and simple implications which enable the verification process to succeed. As long as the implementation circuit is directly synthesized from the reference circuit, such approaches can be successful and have been shown to verify multiplier circuits with multiplicand widths in excess of 64 bits. Unfortunately, multipliers with different architectures do not provide enough structural similarity to allow verification with the these methods.
Architectural changes are common, however, and particularly during the earlier part of the design process. For example, with respect to multipliers, it is common to swap one multiplier architecture for another in order to explore design tradeoffs. As a specific example, it would not be uncommon to substitute an array multiplier (as shown in FIG. 1) for a Wallace-tree multiplier (as shown in FIG. 2), or vice versa.
Across different architectures, there are known methods for verification, but only if the verification tool knows that the circuits to be verified are multipliers and also knows how the integers processed by the multiplier are encoded.
It would therefore be desirable to develop a general technique for formally determining equivalence between circuits of different architectures such that it is not necessary for the verification tool to know the particular functionality of the circuits to be compared nor the specific way in which the operands of the circuits are encoded.
The present invention utilizes a particular type of structural similarity between the reference and implementation designs, which we shall refer to as xe2x80x9cstructural dependence,xe2x80x9d in order to broaden the class of circuits that are formally verifiable in an efficient manner. Structural dependence is the dependence of the higher-order result bits of a design upon the circuitry driving the lower-order result bits.
Because structural dependence is a rather general and high-level characteristic, two circuits which might be considered, according to conventional standards, as having very different structures and therefore not amenable to efficient formal verification, may in fact be efficiently comparable using the present invention.
Structural dependence is utilized in partitioning the two circuits, xcex7 and xcex7xe2x80x2, to be compared. Each circuit has the fanin cones of its primary inputs ordered from smallest to largest. Each such fanin cone is the basis for forming a circuit partition, but part of a fanin cone may be excluded from a partition to the extent it is already part of another partition.
Structural dependence partitioning creates subcircuits xcex7i for circuit xcex7 and subcircuits xcex7xe2x80x2i for circuit xcex7xe2x80x2. Each subcircuit (or partition) xcex7i drives a primary output zi and each subcircuit (or partition) xcex7xe2x80x2i drives a primary output zxe2x80x2i. In addition, each subcircuit xcex7i may have: a fanout set Yi to its higher order subcircuit xcex7i+1, (if it has a higher order subcircuit and is connected to it), inputs from the fanout set Yixe2x88x921 of its lower order subcircuit xcex7ixe2x88x921, (if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs). Likewise, each subcircuit xcex7xe2x80x2i may have: a fanout set Yxe2x80x2i to its higher order subcircuit xcex7xe2x80x2i+1 (if it has a higher order subcircuit and is connected to it), inputs from the fanout set Yxe2x80x2ixe2x88x921 of its lower order subcircuit xcex7xe2x80x2ixe2x88x921 (if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs).
Since the lower order primary output bits have smaller fanin cones with fewer inputs than the higher order bits, they may be verifiable by known techniques. As we proceed toward the higher order bits, however, implicit verification using structural dependence becomes increasingly important.
Implicit verification operates as follows, for example, with respect to verifying the high-order primary output bit of two n bit circuits. While the following discussion is stated with respect to two multiplier circuits being compared, it applies to any two circuits which have been partitioned according to structural dependency.
A condition called C is defined which asserts that the high order primary output bits, of each of the two multipliers being compared, are equivalent. More specifically, condition C asserts that znxe2x88x921=zxe2x80x2nxe2x88x921. At this point we are only considering znxe2x88x921 and zxe2x80x2nxe2x88x921 as being outputs, respectively, of subcircuits xcex7nxe2x88x921 and xcex7xe2x80x2nxe2x88x921.
A condition A is defined which asserts that all the lower-order primary output bits of the two multipliers are equivalent. More specifically, condition A asserts that zi=zxe2x80x2i for 0xe2x89xa6i less than nxe2x88x921. Thus all the remaining subcircuits, xcex70 to xcex7nxe2x88x922 and xcex7xe2x80x20 to xcex7xe2x80x2nxe2x88x922, are being considered in A.
We then try to prove the implication that if A is true then C is true, or mathematically Axe2x86x92C. This is equivalent to showing that the conjunction of A being true and C not being true can never be true, or mathematically Axc2x7{overscore (C)}=0.
Once Axe2x86x92C has been proven true, assuming that condition A is known to be true, it is then known by implication that C is true.
Implicit verification utilizes the fact that it is usually easier to prove the implication Axe2x86x92C than to prove C in isolation, since A being true while C being false usually has many conflicting requirements.
Rather than initially formulating a condition A comprised of asserting all lower order bits (i.e., those bits of lower order than C) as being equivalent, it is often advantageous to begin with an assertion (which shall be referred to as Anxe2x88x922) that just the next lower order bits are equivalent (i.e., znxe2x88x922=zxe2x80x2nxe2x88x922). This more limited assertion may provide sufficient constraints such that the implication Anxe2x88x922xe2x86x92C can be proven. At this point, only subcircuits xcex7nxe2x88x921, xcex7xe2x80x2nxe2x88x921, xcex7nxe2x88x922 and xcex7xe2x80x2nxe2x88x922 are being considered. If Anxe2x88x922 does not provide sufficient constraints, then it can be successively augmented with assertions that the next lower pairs of output bits are equivalent. For example, the next lower pair of output bits to be asserted as equivalent would be znxe2x88x923=zxe2x80x2nxe2x88x923 (which shall be referred to as Anxe2x88x923). At this point only subcircuits xcex7nxe2x88x923 and xcex7xe2x80x2nxe2x88x923 are being added for consideration in addition to the subcircuits xcex7nxe2x88x921, xcex7xe2x80x2nxe2x88x921, xcex7nxe2x88x922 and xcex7xe2x80x2nxe2x88x922 already considered for Anxe2x88x922xe2x86x92C . If the implication Anxe2x88x922xc2x7Anxe2x88x923xe2x86x92C can be proven true, then the next lower pair of output bits (which would result in the implication Anxe2x88x922xc2x7Anxe2x88x923xc2x7Anxe2x88x924xe2x86x92C) need not be considered.
In order to prove a particular condition (or antecedent) A as being true, such that it can be used in conjunction with a proven implication Axe2x86x92C to show that a consequent C is true, it is often advantageous to prove a xe2x80x9cchainxe2x80x9d of implications. The chain of implications typically begins with an implication whose consequent asserts the equivalency of low order output bits and therefore has an antecedent A that is provable by conventional means. Once the implication for the low order output bits has xe2x80x9cfiredxe2x80x9d (i.e., its antecedent has been satisfied), its consequent can be used, in turn, to fire an implication for asserting the equivalency of the next higher-order output bit pair. Similarly, the equivalency of the next higher-order output bit pair can be used to fire an implication for proving equivalency of an even higher-order output bit pair. Such a chain of implication firings continues until all output bits, between the two circuits to be compared, have been shown equivalent.
Advantages of the invention will be set forth, in part, in the description that follows and, in part, will be understood by those skilled in the art from the description or may be learned by practice of the invention. The advantages of the invention will be realized and attained by means of the elements and combinations particularly pointed out in the appended claims and equivalents.